PROOF ONE 

1:	X⊃Y⊃Z BY ASSUMPTION 

2:	X⊃Z⊃Y BY ASSUMPTION 

3:	Y BY ASSUMPTION 

4:	¬ Z BY ASSUMPTION 

5:	X BY ASSUMPTION 

6:	Y⊃Z BY MP(5,1) ASSUMING (5 1) 

7:	Z BY MP(3,6) ASSUMING (3 5 1) 

8:	¬ Z∧Z BY AI(4,7) ASSUMING (4 3 5 1) 

9:	NIL BY TAUT(NIL,8) ASSUMING (4 3 5 1) 

10:	¬ X BY ASSUMPTION 

11:	¬ Z∧Y∧X∧(X⊃Y⊃Z)⊃NIL BY DED(9,4,3,5,1) 

12:	FALSE BY TAUT(FALSE,8) ASSUMING (4 3 5 1) 

13:	¬ Z∧Y∧X∧(X⊃Y⊃Z)⊃FALSE BY DED(12,4,3,5,1) 

14:	¬ (¬ Z∧Y∧X∧(X⊃Y⊃Z)) BY NI 13 

15:	Z∨¬ Y∨¬ X∨¬ (X⊃Y⊃Z) BY TAUT(Z∨¬ Y∨¬ X∨¬ (X⊃Y⊃Z),14) 

16:	Y∧¬ Z∧(X⊃Y⊃Z)⊃¬ X BY TAUT(Y∧¬ Z∧(X⊃Y⊃Z)⊃¬ X,15) 

17:	Z∨¬ Y∨¬ X∨¬ (X⊃Y⊃Z) BY THEOREM HI 

18:	(∀ X) (∀ Z) (Z∨¬ Y∨¬ X∨¬ (X⊃Y⊃Z)) BY UG(17,Z,X) 

19:	(∃ Y) (∀ X) (∀ Z) (Z∨¬ Y∨¬ X∨¬ (X⊃Y⊃Z)) BY EG(18,Y) 

20:	(∀ Z) (Z∨¬ Y∨¬ X∨¬ (X⊃Y⊃Z)) BY US(18,X) 

21:	(∀ X1) (∀ Z) (Z∨¬ X∨¬ X1∨¬ (X1⊃X⊃Z)) BY US(19,X) 

PROOF VALUE 

THEOREM HI 
Z∨¬ Y∨¬ X∨¬ (X⊃Y⊃Z)